/LMAR=0/XLINE=3/FONT#3=BASB30/FONT#2=BASI30/FONT#1=BDR30/FONT#0=BDR30



␈↓ ↓H␈↓␈↓ ↓x␈↓αsamefringe␈↓↓[␈↓αx␈↓↓, ␈↓αy␈↓↓] ← [¬␈↓βat ␈↓αx␈↓↓ ∧ ¬␈↓βat ␈↓αy␈↓↓ ∧ ␈↓αsame␈↓↓[␈↓βa ␈↓αx␈↓↓, ␈↓βa ␈↓αy␈↓↓, ␈↓βd ␈↓αx␈↓↓, ␈↓βd ␈↓αy␈↓↓]] ∨ ␈↓αx␈↓↓ ␈↓βeq ␈↓αy



␈↓ ↓H␈↓α␈↓ ↓xsame␈↓↓[␈↓αx␈↓↓, ␈↓αy␈↓↓, ␈↓αu␈↓↓, ␈↓αv␈↓↓] ←
␈↓ ↓H␈↓↓␈↓ α_[¬␈↓βat ␈↓αx␈↓↓ ∧ ¬␈↓βat ␈↓αy␈↓↓ ∧ ␈↓αsame␈↓↓[␈↓βa ␈↓αx␈↓↓, ␈↓βa ␈↓αy␈↓↓, ␈↓βd ␈↓αx␈↓↓ . ␈↓αu␈↓↓, ␈↓βd ␈↓αy␈↓↓ . ␈↓αv␈↓↓]]
␈↓ ↓H␈↓↓␈↓ α_∨ [¬␈↓βat ␈↓αy␈↓↓ ∧ ␈↓αsame␈↓↓[␈↓αx␈↓↓, ␈↓βa ␈↓αy␈↓↓, ␈↓αu␈↓↓, ␈↓βd ␈↓αy␈↓↓ . ␈↓αv␈↓↓]]
␈↓ ↓H␈↓↓␈↓ α_∨ [¬␈↓βat ␈↓αx␈↓↓ ∧ ␈↓αsame␈↓↓[␈↓βa ␈↓αx␈↓↓, ␈↓αy␈↓↓, ␈↓βd ␈↓αx␈↓↓ . ␈↓αu␈↓↓, ␈↓αv␈↓↓]]
␈↓ ↓H␈↓↓␈↓ α_∨ [␈↓αx␈↓↓ ␈↓βeq ␈↓αy␈↓↓ ∧ ␈↓αsamefringe␈↓↓[␈↓αu␈↓↓, ␈↓αv␈↓↓]]



␈↓ ↓H␈↓↓␈↓ ↓x␈↓αsamefringe1␈↓↓[␈↓αx␈↓↓, ␈↓αy␈↓↓] ← ␈↓αx␈↓↓ ␈↓βeq ␈↓αy␈↓↓ ∨ [¬␈↓βat ␈↓αx␈↓↓ ∧ ¬␈↓βat ␈↓αy␈↓↓ ∧ ␈↓αsame1␈↓↓[␈↓βa ␈↓αx␈↓↓, ␈↓βa ␈↓αy␈↓↓, ␈↓βd ␈↓αx␈↓↓, ␈↓βd ␈↓αy␈↓↓]]



␈↓ ↓H␈↓↓␈↓ ↓x␈↓αsame1␈↓↓[␈↓αx␈↓↓, ␈↓αy␈↓↓, ␈↓αu␈↓↓, ␈↓αv␈↓↓] ←
␈↓ ↓H␈↓↓␈↓ α_␈↓βif␈↓↓ ␈↓βat ␈↓αx␈↓↓ ␈↓βthen␈↓↓ [␈↓βif␈↓↓ ␈↓βat ␈↓αy␈↓↓ ␈↓βthen␈↓↓ ␈↓αx␈↓↓ ␈↓βeq ␈↓αy␈↓↓ ∧ ␈↓αsamefringe1␈↓↓[␈↓αu␈↓↓, ␈↓αv␈↓↓] ␈↓βelse␈↓↓ ␈↓αsame1␈↓↓[␈↓αx␈↓↓, ␈↓βa ␈↓αy␈↓↓, ␈↓αu␈↓↓, ␈↓βd ␈↓αy␈↓↓ . ␈↓αv␈↓↓]]
␈↓ ↓H␈↓↓␈↓ α_␈↓βelse if␈↓↓ ␈↓βat ␈↓αy␈↓↓ ␈↓βthen␈↓↓ ␈↓αsame1␈↓↓[␈↓βa ␈↓αx␈↓↓, ␈↓αy␈↓↓, ␈↓βd ␈↓αx␈↓↓ . ␈↓αu␈↓↓, ␈↓αv␈↓↓]
␈↓ ↓H␈↓↓␈↓ α_␈↓βelse␈↓↓ ␈↓αsame1␈↓↓[␈↓βa ␈↓αx␈↓↓, ␈↓βa ␈↓αy␈↓↓, ␈↓βd ␈↓αx␈↓↓ . ␈↓αu␈↓↓, ␈↓βd ␈↓αy␈↓↓ . ␈↓αv␈↓↓]



␈↓ ↓H␈↓↓␈↓ ↓x␈↓αsamefringe2␈↓↓[␈↓αx␈↓↓, ␈↓αy␈↓↓] ← ␈↓αsame2␈↓↓[␈↓αabot␈↓↓ <␈↓αx␈↓↓>, ␈↓αabot␈↓↓ <␈↓αy␈↓↓>]



␈↓ ↓H␈↓↓␈↓ ↓x␈↓αsame2␈↓↓[␈↓αu␈↓↓, ␈↓αv␈↓↓] ← [␈↓βn ␈↓αu␈↓↓ ∧ ␈↓βn ␈↓αv␈↓↓] ∨ [¬␈↓βn ␈↓αu␈↓↓ ∧ ¬␈↓βn ␈↓αv␈↓↓ ∧ ␈↓βa ␈↓αu␈↓↓ ␈↓βeq a ␈↓αv␈↓↓ ∧ ␈↓αsame2␈↓↓[␈↓αnext␈↓↓ ␈↓αu␈↓↓, ␈↓αnext␈↓↓ ␈↓αv␈↓↓]]



␈↓ ↓H␈↓↓␈↓ ↓x␈↓αnext␈↓↓ ␈↓αu␈↓↓ ← ␈↓βif␈↓↓ ␈↓βn ␈↓αu␈↓↓ ␈↓βthen␈↓↓ NIL ␈↓βelse if␈↓↓ ␈↓βad ␈↓αu␈↓↓ ␈↓βeq ␈↓α'a␈↓↓ ␈↓βthen␈↓↓ ␈↓αabot␈↓↓ ␈↓βdadd ␈↓αu␈↓↓ . [␈↓α'd␈↓↓ . ␈↓βdd ␈↓αu␈↓↓] ␈↓βelse␈↓↓ ␈↓αnext␈↓↓ ␈↓βdd ␈↓αu



␈↓ ↓H␈↓α␈↓ ↓xabot␈↓↓ ␈↓αu␈↓↓ ← ␈↓βif␈↓↓ ␈↓βat a ␈↓αu␈↓↓ ␈↓βthen␈↓↓ ␈↓αu␈↓↓ ␈↓βelse␈↓↓ ␈↓αabot␈↓↓ ␈↓βaa ␈↓αu␈↓↓ . [␈↓α'a␈↓↓ . ␈↓αu␈↓↓]



␈↓ ↓H␈↓↓␈↓ ↓x␈↓αsamefringe3␈↓↓[␈↓αx␈↓↓, ␈↓αy␈↓↓] ←
␈↓ ↓H␈↓↓␈↓ α_␈↓αx␈↓↓ ␈↓βeq ␈↓αy␈↓↓ ∨ [¬␈↓βat ␈↓αx␈↓↓ ∧ ¬␈↓βat ␈↓αy␈↓↓ ∧ {␈↓αdigatom␈↓↓ ␈↓αx␈↓↓, ␈↓αdigatom␈↓↓ ␈↓αy␈↓↓}[λ␈↓αu␈↓↓, ␈↓αv␈↓↓. ␈↓βa ␈↓αu␈↓↓ ␈↓βeq a ␈↓αv␈↓↓ ∧ ␈↓αsamefringe3␈↓↓[␈↓βd ␈↓αu␈↓↓, ␈↓βd ␈↓αv␈↓↓]]]



␈↓ ↓H␈↓↓␈↓ ↓x␈↓αsamefringe4␈↓↓[␈↓αx␈↓↓, ␈↓αy␈↓↓] ← ␈↓αx␈↓↓ ␈↓βeq ␈↓αy␈↓↓ ∨ [¬␈↓βat ␈↓αx␈↓↓ ∧ ¬␈↓βat ␈↓αy␈↓↓ ∧ ␈↓αsame4␈↓↓[␈↓αdigatom␈↓↓ ␈↓αx␈↓↓, ␈↓αdigatom␈↓↓ ␈↓αy␈↓↓]]
␈↓ ↓H␈↓␈↓ j1


␈↓ ↓H␈↓↓␈↓ ↓x␈↓αsame4␈↓↓[␈↓αx␈↓↓, ␈↓αy␈↓↓] ← ␈↓βa ␈↓αx␈↓↓ ␈↓βeq a ␈↓αy␈↓↓ ∧ ␈↓αsamefringe4␈↓↓[␈↓βd ␈↓αx␈↓↓, ␈↓βd ␈↓αy␈↓↓]



␈↓ ↓H␈↓↓␈↓ ↓x␈↓αdigatom␈↓↓ ␈↓αu␈↓↓ ← ␈↓βif␈↓↓ ␈↓βat a ␈↓αu␈↓↓ ␈↓βthen␈↓↓ ␈↓αu␈↓↓ ␈↓βelse␈↓↓ ␈↓αdigatom␈↓↓ ␈↓βaa ␈↓αu␈↓↓ . [␈↓βda ␈↓αu␈↓↓ . ␈↓βd ␈↓αu␈↓↓]